; COMMAND-LINE: --learned-rewrite
; EXPECT: sat
(set-logic QF_ABV)
(declare-const __ (_ BitVec 1))
(define-fun x () (_ BitVec 16) ((_ zero_extend 15) __))
(declare-const x1 Bool)
(declare-fun x2 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x22 () (_ BitVec 768))
(declare-fun p () Bool)
(assert (= (select x2 (_ bv0 5)) ((_ extract 415 384) x22)))
(assert (= (select x2 (_ bv0 5)) ((_ extract 383 352) x22)))
(assert (= (select x2 (_ bv0 5)) ((_ extract 351 320) x22)))
(assert (= (select x2 (_ bv0 5)) ((_ extract 319 288) x22)))
(assert (= (select x2 (_ bv0 5)) (_ bv1 32)))
(assert (= (select x2 (_ bv0 5)) ((_ extract 255 224) x22)))
(assert (= (select x2 (_ bv0 5)) ((_ extract 223 192) x22)))
(assert (= (_ bv0 32) (select x2 (_ bv1 5))))
(assert (= x1 (and p (bvsle (_ bv1 32) ((_ zero_extend 16) x)))))
(assert x1)
(assert (= p (bvsle (_ bv0 32) ((_ zero_extend 16) ((_ zero_extend 15) __)))))
(check-sat)
